A:Type, eq:EqDecider(A), B:(AType), f:fpf(A; a.B(a)), x:A, v:B(x).
fpf-compatible(A; a.B(a); eq; f; fpf-single(x; v))
 ((fpf-dom(eq; x; f))  (v = fpf-ap(f; eq; x))) 

latex

Definitions	t  T, top, x(s), P  Q, x:A. B(x), x. t(x), fpf(A; a.B(a)), fpf-single(x; v), fpf-dom(eq; x; f), b, prop{i:l}, P  Q, fpf-ap(f; eq; x), fpf-compatible(A; a.B(a); eq; f; g), EqDecider(T), P  Q, P  Q
Lemmas	subtype rel self, fpf-single-dom-sq, deq property, fpf-compatible wf, fpf-ap wf, fpf wf, deq wf, assert wf, fpf-dom wf, fpf-single wf, top wf, fpf-trivial-subtype-top